the_w:World, i:Id, a:Action(i). isnull(a)  val(a)  valtype(i;a) 

latex

Definitions	World, isnull(a), Action(i), valtype(i;a), val(a), kind(a), w.TA, w.M, Action(dec), outr(x), False, True, w-action-dec(TA;M;i), Knd, kindcase(k; a.f(a); l,t.g(l;t) ), islocal(k), act(k), lnk(k), tag(k), Unit, P  Q, P & Q, P  Q, a = b, destination(l), 1of(t), , Prop, b, A, b, t  T, 2of(t), Id, IdLnk, x. t(x), x:A. B(x)
Lemmas	pi2 wf, assert wf, not wf, bnot wf, subtype rel self, bool wf, Id wf, IdLnk wf, pi1 wf, ldst wf, eq id wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, world wf, w-action wf, w-isnull wf